Inference at * 
Iof proof for Lemma or functionality wrt iff:


  P1,P2,Q1,Q2:. (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2)) 

latex

 by ((GenUnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. P1 : 
C1: 2. P2 : 
C1: 3. Q1 : 
C1: 4. Q2 : 
C1: 5. P1  P2
C1: 6. Q1  Q2
C1: 7. P1  Q1
C1:   P2  Q2
C2: 

C2: 1. P1 : 
C2: 2. P2 : 
C2: 3. Q1 : 
C2: 4. Q2 : 
C2: 5. P1  P2
C2: 6. Q1  Q2
C2: 7. P2  Q2
C2:   P1  Q1
C.

Definitions	t  T, P  Q, P  Q, P  Q, P  Q, P  Q, , x:A. B(x)
Lemmas	iff wf